Tsinghua and Wharton researchers use GPT-built proof to set a limit on gradient descent step sizes

Researchers Jianhao Ma of Tsinghua University and Yuxin Chen of the University of Pennsylvania’s Wharton School have released a paper addressing a roughly 40-year question in optimization theory: how far standard gradient descent can go if its structure is left unchanged and only the step-size schedule is tuned. Their result states that for any pre-specified nonnegative step-size sequence, gradient descent has a lower-bound convergence rate of Ω(T^-1.9319), ruling out the possibility that step-size design alone can match the O(1/T²) rate achieved by Nesterov’s accelerated method. The paper, as described in the report, is notable not only for the theorem itself but also for how the proof was produced. The core argument was generated through iterative work with GPT-5.6 Sol Pro, with the researchers supplying the problem target and a high-level “resisting oracle” strategy, then correcting gaps as they appeared. The result was later translated into Lean 4 code with Codex and formally checked line by line. According to the report, the final formalization used zero “sorry” and zero “admit,” meaning no proof steps were skipped. The code has been made public on GitHub alongside a traceability file linking the paper’s theorems to the Lean implementation.